$M$.ef($k$,$x$,$s$,$v$)?$w$ $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$1of(2of(2of(2of(2of($M$)))))($\langle$$k$$,\,$$x$$\rangle$)?$\lambda$$s$,$v$. $w$($s$,$v$)